Nuprl Lemma : f2f+Owes_wf
11,40
postcript
pdf
es
:ES,
ff
:FIFO,
f2f+
:F2F+-decls. owes_ack
Id
Id
Id
latex
Definitions
ES
,
t
T
,
x
:
A
.
B
(
x
)
,
FIFO
,
F2F+-decls
,
owes_ack
,
x
:
A
B
(
x
)
,
x
:
A
B
(
x
)
,
Id
Lemmas
F2F+-decls
wf
,
FIFO
wf
,
event
system
wf
origin
es:ES, ff:FIFO, f2f+:F2F+-decls. owes_ack 
Id
IdId es:ES, ff:FIFO, f2f+:F2F+-decls. owes_ack IdIdId Tx:A. B(x)
B(x)B(x)